Inference at * 1 
Iof proof for Lemma decidable-filter:



1. T : Type
2. T List
3. P : {x:T| (x  [])} 
4. x[]. Dec(P(x))
  L':T List. (L'  [] & (x:T. (x  L')  ((x  []) & P(x)))) 

latex

 by ((InstConcl [[]]) 
CollapseTHEN (MaAuto)) 

latex

C1: 

C1:   []  []
C.

Definitions	[], suptype(S; T), #$n, {i..j}, i  j < k, P  Q, P  Q, P & Q, A c B, S  T, |g|, l[i], , , A  B, A, False, Void, ||as||, x(s), a < b, increasing(f;k), x:A. B(x), x:A  B(x), Dec(P), P  Q, P  Q, left + right, L1  L2, xL. P(x), type List, f(a), {x:A| B(x)} , x:A. B(x), x:AB(x), (x  l), s = t, t  T, , Type
Lemmas	nil member, increasing wf, length wf1, int seg wf, le wf, sublist wf, rev implies wf, member wf, subtype rel wf, iff wf, nat wf, length wf2, select wf, l member wf